build: warn when bin/hol or bin/unquote is older than its sources - #2037
Open
lukaszcz wants to merge 5 commits into
Open
build: warn when bin/hol or bin/unquote is older than its sources#2037lukaszcz wants to merge 5 commits into
lukaszcz wants to merge 5 commits into
Conversation
The quote filter's lexer is generated from tools/parsing/HolLex by configure, and by no Holmakefile rule, so pulling a grammar change into an existing tree leaves the old bin/unquote in place. It then mis-lexes the new syntax, and the failure surfaces a long way from its cause: a lex error part way through some theory build, with nothing pointing at the filter or at the need to reconfigure. build already defends against this class of staleness -- check_against on the configure scripts and on build itself, plus a sweep of every .sml file under tools/Holmake against the Holmake binary -- but none of those reach HolLex, which has no .sml extension and does not live under tools/Holmake. Check it explicitly, raising the same "this suggests you should reconfigure the system" prompt as the existing guards, and only when bin/unquote is actually present so that a tree which has not been configured yet is unaffected. Both build front ends get the check, tools/build for Moscow ML and tools-poly for Poly/ML, each in the idiom the surrounding file already uses for its filesystem calls.
bin/hol is compiled by configure from tools-poly/hol.ML and the Holmake sources it links against, and by no Holmakefile rule, so pulling into an existing tree leaves it stale with nothing to say so. The guards already in build do not reach it. check_against covers the configure scripts, build itself and Systeml.sig; the app_sml_files sweep covers tools/Holmake and tools-poly/Holmake but compares them against bin/Holmake, so a tree whose Holmake was regenerated can still run a hol built from quite different sources. hol.ML is covered by nothing at all. This is not hypothetical. 1821cc3 moved the Meta.loadPath extension in hol.ML from before loadState to after, because the state load restores refs to their save-time values and was wiping it, and removed prelude.ML's compensating re-extension in the same commit. A tree carrying the old bin/hol therefore got neither: loadPath stayed at the bare [sigobj], so interactive load and open could not see INCLUDES directories, and the banner prelude prints when the path grows never fired. All six tools/Holmake/tests/repl tests failed against their expected output. That last part is what makes it expensive. repl is a test-only entry in sequences/kernel, so -t reaches it while still inside the kernel sequence, and the failure aborts the build there. Since build cleans and re-uploads sigobj per entry, aborting that early strands every library from src/marker onward, and per-directory Holmake in an affected directory then fails with a name resolution error in unmodified source. Nothing in that symptom points at bin/hol, or at reconfiguring. Poly only: under Moscow ML bin/hol is a shell script emitted by configure, not a compiled artefact, so tools/build/build.sml has nothing to check.
Member
|
Poly/ML HOL does not run |
Under Poly/ML nothing runs bin/unquote: emit_hol_unquote_script is a no-op there, and the filter's lexer and parser are instead linked into bin/Holmake and bin/hol via hmcore.ML. A stale bin/unquote therefore breaks no build, while the binaries that do mis-lex a pulled grammar change went unchecked -- and the exposure is wider than HolLex, since the HOLSource* and AttributeSyntax sources in tools/parsing are baked in the same way and swept by nothing. So drop the unquote check from tools-poly/build.sml and instead check tools/parsing against bin/hol in its existing check block: HolLex explicitly (no .sml extension), the rest by app_sml_files sweep. Checking hol alone covers Holmake's embedded copy too, because configure builds Holmake before hol -- a bin/hol current with respect to tools/parsing implies a bin/Holmake from the same run or a later one. tools/build/build.sml is unchanged: under Moscow ML unquote genuinely runs as a pipe filter, so its check stands.
The comment's opening "likewise" pointed at the bin/unquote check block deleted in the previous commit, and the tools/parsing rationale trailed as a separate paragraph. Fold both into one self-contained block.
lukaszcz
changed the title
Contributor
Author
Now for Poly/ML it checks |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
Several
bin/binaries are compiled byconfigureand by no Holmakefile rule, so pulling in a source change leaves them stale and silently wrong.build.smlguards this class of staleness withcheck_against, but its sweep only covers.smlfiles undertools/Holmakeandtools-poly/Holmake, compared againstbin/Holmake. Three gaps:bin/unquoteruns as a pipe filter and mis-lexes new syntax whentools/parsing/HolLexchanges.HolLexhas no.smlextension and is not under aHolmakedirectory, so the sweep misses it.bin/unquote(emit_hol_unquote_scriptis a no-op); the filter is linked intobin/Holmakeandbin/holviahmcore.ML. So a staleunquotebreaks nothing, while the binaries that do mis-lex go unchecked — and not just forHolLex:HOLSource*andAttributeSyntaxintools/parsingare baked in the same way.bin/holat all.tools-poly/hol.MLis swept by nothing, and a tree with a currentbin/Holmakecan still run aholbuilt from other sources. A staleholmisdirects the interactive load path and failstools/Holmake/tests/repl, which-treaches insidesequences/kernel— halting the selftest build.Change
tools/build/build.sml(mosml): checkbin/unquoteagainsttools/parsing/HolLex.tools-poly/build.sml(Poly/ML): checkbin/holagainst everything linked into it —tools-poly/hol.ML, the twoHolmakesweeps,tools/parsing/HolLexexplicitly, and anapp_sml_filessweep oftools/parsing. Nounquotecheck, which is not in the loop here. Checkingholcovers Holmake's embedded filter too:configurebuildsHolmakefirst.Both follow the existing check's shape — fire only if the executable is present, and warn ("you should reconfigure the system", Ctrl-C or RETURN) rather than fail.
Notes
bin/Holmakecheck.